package propcalc_lang.ast;

import java.util.*;

/** Categoría sintáctica de las proposiciones, i.e. fórmulas bien formadas en el
 *  cálculo proposicional. Todas las clases que representan construcciones 
 *  dentro de la categoria deben heredar de esta clase.
 *  @author Leonardo Val.
 */
public abstract class Proposition extends Formula {

	/** Genera una instancia aleatoria de Proposition. 
	 */
	public static Proposition generate(Random random, int min, int max) {
		int i = min > 0 ? random.nextInt(6) + 2 : 
			max > 0 ? random.nextInt(8) : 
			random.nextInt(2);
		switch (i) {
			case 0: return TruthValue.generate(random, min, max);
			case 1: return Variable.generate(random, min, max);
			case 2: return Negation.generate(random, min, max);
			case 3: return Conjunction.generate(random, min, max);
			case 4: return Disjunction.generate(random, min, max);
			case 5: return ExclusiveDisjunction.generate(random, min, max);
			case 6: return Conditional.generate(random, min, max);
			default: return Biconditional.generate(random, min, max);
		}
	}
	
	/** Agrega al Set dado las variables en la fórmula y lo retorna.
	 */
	public abstract Set<String> variables(Set<String> vars);
	
	/** Retorna una nueva proposición igual a ésta, pero con las variables 
	 *  sustituídas por las proposiciones dadas en replacements. 
	 */
	public abstract Proposition substitution(Map<String, Proposition> replacements);
	
	/** Verifica si es posible obtener un conjunto de reemplazos que permita
	 *  obtener a esta proposición mediante una sustitución de pattern.
	 */
	public abstract boolean match(Proposition pattern, Map<String, Proposition> replacements);
}
